1. Field of the Invention
The present invention relates in general to verifying designs and in particular to representing a logic function in a decision diagram. Still more particularly, the present invention relates to a system, method and computer program product for building binary decision diagrams more optimally using don't-caring.
2. Description of the Related Art
Many tasks in computer-aided design (CAD) of digital circuits, such as equivalence checking, property checking, logic synthesis, false-paths analysis require Boolean reasoning on problems derived from circuit structures. A netlist graph is a means of representing problems derived from these circuit structures. Such a representation is non-canonical and offers limited ability to reason about the function at the nodes in the graph. Binary decision diagrams (BDDs) can be used for efficiently applying Boolean reasoning to problems derived from such circuit structures. BDDs offer a compact and functionally canonical representation of the Boolean function of a graph node, which makes it easy and fast to reason about its function. Unfortunately, the size of BDDs and hence the complexity involved with manipulating them is very sensitive to the order in which variables appear in the BDDs. This sensitivity to variable ordering can result in exponential space complexity of the BDD in the worst case. BDD packages that implement BDD building and manipulation algorithms use Dynamic Variable Ordering (DVO) algorithms to reduce the number of BDD nodes periodically. These algorithms tend to be expensive in both time and space complexity. Therefore BDD software packages rely on heuristics to compute a local minimum as opposed to a global minimum for reducing the number of BDD nodes, since computing a global minimum is prohibitively expensive.
In such an approach a set of nodes for which BDDs are required to be built, called “sink” nodes, are identified. Examples of sink nodes are outputs in an equivalence checking or false-paths analysis setting, or targets in a property checking or model checking setting. Next, BDDs for these nodes are obtained by building BDDs in a topological manner, starting at the inputs, for intermediate nodes in the circuit graph representation until the BDDs for the sink nodes are built.
Typical techniques use either a depth-first or a breadth-first approach to build BDDs topologically for sink nodes starting at the inputs. This process tends to suffer from an exponential space and hence time complexity in the worst case often times precluding BDDs for the sink nodes from being built at all. One reason for this blow-up is the (large) size of the intermediate BDDs required to be built in order to obtain the BDDs for the sink nodes. This results in a prohibitively large number of “alive” BDD nodes. A BDD is said to be alive if it is still needed to build BDDs for its fanout nodes. Thus, there is a need in the art for a technique of building BDDs that manages available resources efficiently by attempting to minimize the number of live BDDs and thereby reducing overall memory consumption.